\appsection{Weighted Partial Max-SAT}
\label{appendix:maxsat}

%In our first approach for solving the MinCost SAT problem, we
We introduce how to convert a MinCost SAT problem into a weighted partial Max-SAT
instance in this appendix.
%, and then apply an existing Max-SAT solver to solve the instance.
% The reason of doing this is mostly because of the wide popularity
%of MaxSAT solvers nowadays.
We first introduce the definition of
%Another extended SAT problem that we consider is the 
weighted partial Max-SAT Problem~\cite{maxsat09}.

\begin{defn}\em (Weighted partial Max-SAT problem)~\label{def:maxsat}
A weighted partial Max-SAT problem is a tuple
$\Phi^{a}=(V,C^h,C^s,w)$,  where $V$ is a set of variables, $C^h$
and $C^s$ are sets of hard and soft clauses, respectively, and $w$ is the weight function
of soft clauses defined by $w: C^s \rightarrow \mathbb{N}$.

A solution to $\Phi^{a}$ is a variable assignment $\psi$ that maximizes the function:
$$ weight(\psi) = \sum_{\forall p \in {C^s}}{w(p)v_{\psi}(p)},$$
\hspace{16mm}subject to: $v_{\psi}(p)=1,\forall p\in C^h.$
\end{defn}


A weighted partial Max-SAT problem $\Phi^a$ amounts to
finding a variable assignment, such that all hard
clauses are satisfied, and the total weight of satisfied soft
clauses is maximized.

Given a MinCost SAT instance $\Phi^{c}=(V,C,\mu)$, we construct a
weighted partial Max-SAT instance $\Phi^{a}=(V,C,C^s,w)$.
% with the same $V$.
The hard clause set is equivalent to the clause set in the original
MinCost SAT problem. The soft clause set $C^s$ is constructed as:
%$$C^s=\{x_j\} \bigcup \{ \neg x_j\}, \forall x_j \in V.$$
$$C^s = \{ \neg x \mid x\in V \}.$$
For each clause $p \in C^s$, its weight is consequently defined as:
$$w(p) = \mu(x),~where~p=\neg x.$$
\nop{
\[ w(p) = \left  \{
\begin{array}{ll}
    \mu(x),       & \mbox{if $p \in C^s$, $p=\neg x$ } \\
    \infty,     & \mbox{if $p \in C^h$}\\
\end{array} \right. \]
} According to  Definition~\ref{def:maxsat}, given a variable
assignment $\psi$, the objective function of the weighted partial
Max-SAT instance is:
\begin{align*}
weight(\psi)  & = \sum_{\forall p \in {C^s}}{w(p)v_{\psi}(p)}\\
           & = \sum_{\forall x \in V}{\mu(x)v_{\psi}(\neg x)}~(\because C^s = \{ \neg x \mid x\in V \} )\\
           & = \sum_{\forall x \in V}{\mu(x)(1-v_{\psi}( x))}\\
           & = \sum_{\forall x \in V}{\mu(x)} - \sum_{\forall x \in V}{\mu(x)v_{\psi}(x)}\\
           & = \sum_{\forall x \in V}{\mu(x)} - cost(\psi).
\end{align*}
Hence, maximizing $weight(\psi)$ is equivalent to minimizing $cost(\psi)$.
Since $cost(\psi)$ is the objective function of the MinCost SAT problem
$\Phi^{c}$, solving a MinCost SAT problem is equivalent to solving
the constructed weighted partial Max-SAT problem $\Phi^a$.

%In our experiments, we use a state-of-the-art
%Max-SAT solver, SAT-4j, the winner of weighted partial Max-SAT (Industrial) domain in Max-SAT 2009 competition.%

For example, given a MinCost SAT problem $\Phi^{c}=(V,C,\mu)$ as
follows:
\begin{align*}
C:~& x_1~ \vee~ x_2      &c:~   &  \mu(x_1)=5 \\
   & x_2~ \vee~ \neg x_3 &      &  \mu(x_2)=10\\
   &                     &      &  \mu(x_3)=7\\
\end{align*}
The corresponding weighted partial Max-SAT problem
$\Phi^a=(V,C^h,C^s,w)$ is:
%\begin{align*}
%C^h:~& \infty~ x_1~\vee~x_2     & C^s:~& 0~ x_1\\
%     & \infty~ x_2~\vee~\neg x_3&      & 5~ \neg x_1 \\
%     &                          &      & 0~ x_2\\
%     &                          &      & 10~ \neg x_2\\
%     &                          &      & 0~ x_3\\
%     &                          &      & 7~ \neg x_3\\
%\end{align*}
\begin{align*}
     &  Clause  & w(p) \\
C^h:~& x_1~\vee~x_2      & \infty\\
     & x_2~\vee~\neg x_3 & \infty \\
C^s:~& \neg x_1  & 5\\
     & \neg x_2 & 10\\
     & \neg x_3   & 7\\
\end{align*}
The optimal solution to $\Phi^{c}$ is $v_{\psi}(x_1)=1$, $v_{\psi}(x_2)=0$,
$v_{\psi}(x_3)=0$, and the objective function $cost(\psi)=5$. The optimal
solution to $\Phi^{a}$ is the same $\psi$, and $weight(\psi)= 17$. By
solving any of the two problems, we have the solution to the other problem. 
\nop{
Since Max-SAT has been extensively studied~\cite{Xing05maxsolver,Fu06b,Li07,Robinson10}, we can make use
of the existing Max-SAT solvers, such as SAT4J~\cite{sat4j}, IncWMaxSatz~\cite{Darras07}, W-MaxSatz~\cite{Li06,Li07,Li09} and 
Clone~\cite{Pipatsrisawat07clone}, to tackle our MinCost SAT formulation.
}
%They have the same variable assignment and the
%objective functions :
%$weight(v)=\mu(x_1)+\mu(x_2)+\mu(x_3)}-cost(V)$.

% R.Huang Without partial order stuff, this Proof is unnecessary any more.
%\begin{theorem} {\em (Optimality)}
%The STEP algorithm in Algorithm~\ref{overall} always finds the
%solution with the minimal time span, if such a solution exists.
%\end{theorem}
%
%Starting with 0, each iteration of Algorithm~\ref{overall} increases
%the time span by $\delta$, and then encodes and solves the SAT
%instance. Therefore, if there exists a solution with the minimal
%time span, Algorithm~\ref{overall} will always find it as the first
%solution it encounters. The partial order of goal variables is
%enforced in the SAT solver so that the first solution found will
%give the minimum time span. Therefore, Algorithm~\ref{overall} is
%optimal in total time span.
